package edu.uclm.combTest.core.pairwise;

import java.util.Iterator;

import edu.uclm.combTest.core.Set;
import edu.uclm.combTest.core.Vector;

public class PairsTable {
	protected /*@ spec_public @*/ Vector pairs;
	/**
	 * Index of a set or other
	 */
	protected /*@ spec_public @*/ int indexA;
	protected /*@ spec_public @*/ int indexB;

	//@ invariant indexA >=0;
	
	//@invariant indexB>=0;
	
	public PairsTable() {
		this.pairs = new Vector();
	}

	/**
	 * Construit toute les paires depuis les 2 sets donnés en paramettre.
	 * @param a
	 * @param b
	 */
	//@ensures pairs.size()==a.size()*b.size();
	//@ensures (
	//@ \forall int i ; i >=0 && i < a.size() ; (
	//@		\forall int j ; j >= 0 && j < b.size() ; (
	//@			pairs.contains(new Pair(i,j)) 
	//@ )));
	public PairsTable(Set a, Set b) {
		this();
		for (int i = 0; i < a.size(); i++) {
			for (int j = 0; j < b.size(); j++) {
				Pair p = new Pair(i, j);
				this.pairs.add(p);
			}
		}
	}
	
	//@ensures (
	//@ \forall int i ; i >=0 && i < pairs.size() ; (
	//@ \result.contains(pairs.get(i))
	//@));
	public /*@ pure @*/ Vector getPairs() {
		return pairs;
	}

	//@ensures indexA == a;
	public void setIndexA(int a) {
		this.indexA = a;
	}
	
	//@ensures indexB == b;
	public void setIndexB(int b) {
		this.indexB = b;
	}

	/**
	 * Renvois une pair du poid donné, ou null si le poid n'est pas trouvé.
	 * @param weight
	 * @return
	 */
	//@requires weight >=0 && (\exists int i ; i>=0 && i < pairs.size() ; ((Pair)pairs.get(i)).weight()==weight);
	//@ensures \result.weight() == weight ;
	//@also 
	//@requires weight >=0 && !(\exists int i ; i>=0 && i < pairs.size() ; ((Pair)pairs.get(i)).weight()==weight);
	//@ensures \result == null;
	public /*@ nullable @*/ Pair getPairWithWeight(int weight) {
		for (Iterator iterator = pairs.iterator(); iterator.hasNext();) {
			Pair p = (Pair) iterator.next();
			if (p.weight == weight)
				return p;
		}
		return null;
	}

	public /*@ pure @*/ int getIndexA() {
		return indexA;
	}

	public /*@ pure @*/ int getIndexB() {
		return indexB;
	}

	/**
	 * Augmente le poid d'une paire
	 * @param a indice de l'element 1
	 * @param b indice de l'element 2.
	 */
	/*@
	 @ requires (\exists int i ; i >=0 && i < pairs.size() ;
	 @ ((Pair)pairs.elementAt(i)).getA() == a &&
	 @ ((Pair)pairs.elementAt(i)).getB() ==b
	 @);
	 @*/
	/*@
	 @ ensures (\exists int i ; i >=0 && i < pairs.size() ;
	 @ ((Pair)pairs.elementAt(i)).weight() == 
	 @ \old(((Pair)pairs.elementAt(i)).weight() +1)
	 @);
	 @*/
	public void increaseWeightOfPair(long a, long b) {
		for (int i = 0; i < this.pairs.size(); i++) {
			Pair p = (Pair) this.pairs.get(i);
			if (p.getA() == a && p.getB() == b) {
				p.increaseWeight();
				return;
			}
		}
	}

	/*@
	 @ requires (\exists int i ; i >=0 && i < pairs.size() ;
	 @ ((Pair)pairs.elementAt(i)).getA() == a &&
	 @ ((Pair)pairs.elementAt(i)).getB() ==b
	 @);
	 @*/
	/*@
	 @ ensures (!(\exists int i ; i >=0 && i < pairs.size() ;
	 @ ((Pair)pairs.elementAt(i)).getA() == a &&
	 @ ((Pair)pairs.elementAt(i)).getB() ==b
	 @));
	 @*/
	/*@
	 @ ensures pairs.size() == \old(pairs.size()-1);
	 @*/
	public void removePair(long a, long b) {
		for (Iterator iterator = pairs.iterator(); iterator.hasNext();) {
			Pair p = (Pair) iterator.next();
			if (p.getA() == a && p.getB() == b) {
				this.pairs.remove(p);
				return;
			}
		}
	}

	/*@
	 @ requires (\exists int i ; i >=0 && i < pairs.size() ;
	 @ ((Pair)pairs.elementAt(i)).getA() == a &&
	 @ ((Pair)pairs.elementAt(i)).getB() ==b
	 @);
	 @*/
	/*@
	 @ ensures (\forall int i ; i >=0 && i < pairs.size() ; 
	 @	(( ((Pair)pairs.elementAt(i))).getA() == a && ((Pair)pairs.elementAt(i)).getB() ==b) 
	 @  ==> ((Pair)pairs.elementAt(i)).weight() == \result.weight
	 @ );
	 @*/
	public /*@ pure @*/ Pair getPair(long a, long b) {
		for (Iterator iterator = pairs.iterator(); iterator.hasNext();) {
			Pair p = (Pair) iterator.next();
			if (p.a == a && p.b == b)
				return p;
		}
		return null;
	}

}
